lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
fac(x) → loop(x, s(0), s(0))
loop(x, c, y) → if(lt(x, c), x, c, y)
if(false, x, c, y) → loop(x, s(c), times(y, s(c)))
if(true, x, c, y) → y
↳ QTRS
↳ DependencyPairsProof
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
fac(x) → loop(x, s(0), s(0))
loop(x, c, y) → if(lt(x, c), x, c, y)
if(false, x, c, y) → loop(x, s(c), times(y, s(c)))
if(true, x, c, y) → y
TIMES(s(x), y) → PLUS(y, times(x, y))
LT(s(x), s(y)) → LT(x, y)
FAC(x) → LOOP(x, s(0), s(0))
IF(false, x, c, y) → LOOP(x, s(c), times(y, s(c)))
LOOP(x, c, y) → IF(lt(x, c), x, c, y)
IF(false, x, c, y) → TIMES(y, s(c))
LOOP(x, c, y) → LT(x, c)
TIMES(s(x), y) → TIMES(x, y)
PLUS(s(x), y) → PLUS(x, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
fac(x) → loop(x, s(0), s(0))
loop(x, c, y) → if(lt(x, c), x, c, y)
if(false, x, c, y) → loop(x, s(c), times(y, s(c)))
if(true, x, c, y) → y
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
TIMES(s(x), y) → PLUS(y, times(x, y))
LT(s(x), s(y)) → LT(x, y)
FAC(x) → LOOP(x, s(0), s(0))
IF(false, x, c, y) → LOOP(x, s(c), times(y, s(c)))
LOOP(x, c, y) → IF(lt(x, c), x, c, y)
IF(false, x, c, y) → TIMES(y, s(c))
LOOP(x, c, y) → LT(x, c)
TIMES(s(x), y) → TIMES(x, y)
PLUS(s(x), y) → PLUS(x, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
fac(x) → loop(x, s(0), s(0))
loop(x, c, y) → if(lt(x, c), x, c, y)
if(false, x, c, y) → loop(x, s(c), times(y, s(c)))
if(true, x, c, y) → y
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
PLUS(s(x), y) → PLUS(x, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
fac(x) → loop(x, s(0), s(0))
loop(x, c, y) → if(lt(x, c), x, c, y)
if(false, x, c, y) → loop(x, s(c), times(y, s(c)))
if(true, x, c, y) → y
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(s(x), y) → PLUS(x, y)
The value of delta used in the strict ordering is 4.
POL(PLUS(x1, x2)) = (4)x_1
POL(s(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
fac(x) → loop(x, s(0), s(0))
loop(x, c, y) → if(lt(x, c), x, c, y)
if(false, x, c, y) → loop(x, s(c), times(y, s(c)))
if(true, x, c, y) → y
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
TIMES(s(x), y) → TIMES(x, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
fac(x) → loop(x, s(0), s(0))
loop(x, c, y) → if(lt(x, c), x, c, y)
if(false, x, c, y) → loop(x, s(c), times(y, s(c)))
if(true, x, c, y) → y
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TIMES(s(x), y) → TIMES(x, y)
The value of delta used in the strict ordering is 4.
POL(TIMES(x1, x2)) = (4)x_1
POL(s(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
fac(x) → loop(x, s(0), s(0))
loop(x, c, y) → if(lt(x, c), x, c, y)
if(false, x, c, y) → loop(x, s(c), times(y, s(c)))
if(true, x, c, y) → y
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
LT(s(x), s(y)) → LT(x, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
fac(x) → loop(x, s(0), s(0))
loop(x, c, y) → if(lt(x, c), x, c, y)
if(false, x, c, y) → loop(x, s(c), times(y, s(c)))
if(true, x, c, y) → y
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LT(s(x), s(y)) → LT(x, y)
The value of delta used in the strict ordering is 12.
POL(s(x1)) = 4 + (2)x_1
POL(LT(x1, x2)) = (3)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
fac(x) → loop(x, s(0), s(0))
loop(x, c, y) → if(lt(x, c), x, c, y)
if(false, x, c, y) → loop(x, s(c), times(y, s(c)))
if(true, x, c, y) → y
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
IF(false, x, c, y) → LOOP(x, s(c), times(y, s(c)))
LOOP(x, c, y) → IF(lt(x, c), x, c, y)
lt(0, s(x)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
fac(x) → loop(x, s(0), s(0))
loop(x, c, y) → if(lt(x, c), x, c, y)
if(false, x, c, y) → loop(x, s(c), times(y, s(c)))
if(true, x, c, y) → y